<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>MdDontHighlightCode</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">## MdDontHighlightCode

</a><a id="25" class="Markup">```agda
</a><a id="33" class="Keyword">module</a> <a id="40" href="MdDontHighlightCode.html" class="Module">MdDontHighlightCode</a> <a id="60" class="Keyword">where</a>
<a id="66" class="Keyword">open</a> <a id="71" class="Keyword">import</a> <a id="78" href="Agda.Builtin.String.html" class="Module">Agda.Builtin.String</a>
<a id="98" class="Markup">```
</a><a id="102" class="Background">
### Marisa

&gt; Sure, but you&#39;re still just a tanuki,	right?
&gt; The kind that drums on their bellies on the night of the full moon,	right?

</a><a id="240" class="Markup">```agda
</a><a id="248" class="Keyword">module</a> <a id="TenDesires"></a><a id="255" href="MdDontHighlightCode.html#255" class="Module">TenDesires</a> <a id="266" class="Keyword">where</a>
  <a id="274" class="Keyword">record</a> <a id="TenDesires.Marisa"></a><a id="281" href="MdDontHighlightCode.html#281" class="Record">Marisa</a> <a id="288" class="Symbol">:</a> <a id="290" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="294" class="Keyword">where</a>
    <a id="304" class="Keyword">constructor</a> <a id="TenDesires.MkSasa"></a><a id="316" href="MdDontHighlightCode.html#316" class="InductiveConstructor">MkSasa</a>
    <a id="327" class="Keyword">field</a>
<a id="333" class="Markup">```
</a><a id="337" class="Background">
### Mamizou

&gt; You are making light of us, are you not? What do you call yourself?

</a><a id="422" class="Markup">```agda
</a>      <a id="TenDesires.Marisa.name"></a><a id="436" href="MdDontHighlightCode.html#436" class="Field">name</a> <a id="441" class="Symbol">:</a> <a id="443" href="Agda.Builtin.String.html#335" class="Postulate">String</a>
<a id="450" class="Markup">```
</a><a id="454" class="Background">
### Marisa

&gt; I&#39;m Reimu Hakurei!

</a><a id="489" class="Markup">```agda
</a><a id="497" class="Keyword">open</a> <a id="502" href="MdDontHighlightCode.html#255" class="Module">TenDesires</a>
<a id="513" class="Keyword">open</a> <a id="518" href="MdDontHighlightCode.html#281" class="Module">Marisa</a>
<a id="525" href="MdDontHighlightCode.html#525" class="Function">_</a> <a id="527" class="Symbol">=</a> <a id="529" href="MdDontHighlightCode.html#316" class="InductiveConstructor">MkSasa</a> <a id="536" class="String">&quot;Reimu Hakurei&quot;</a>
<a id="552" class="Markup">```
</a><a id="556" class="Background">
### Mamizou

&gt; Marisa Kirisame, is it? I&#39;ll be sure to remember that.
&gt; I intend to take my revenge, so you&#39;d best watch your back on the night of the full moon.
</a></pre></body></html>